FDL - Step of Proof: fseg_select

Step of Proof: fseg_select

Inference at * 1 2
Iof proof for Lemma fseg select:

.....wf..... NILNIL

1. T : Type
2. l1 : T List
3. l2 : T List
4. L : T List
5. l2 = (L @ l1)
6. i :

7. i < ||l1||
8. z : T List
9. z = (L @ l1)

(l1[i] = z[((||z|| - ||l1||)+i)])

by ((Auto)

CollapseTHEN (((((if (first_bool T:b) then HypSubst' else RevHypSubst') ( -1)( 0))

)

CollapseTHEN (((RWO "length_append" 0)

CollapseTHEN (Auto'))

))

))

C.

Definitions l[i], -n, A List, [], Top, x:A.B(x), Void, S T, |g|, T, True, #$n, i j , [car / cdr], SQType(T), , A B, A, False, {T}, s ~ t, {x:A| B(x)} , , type List, Type, t T, , n+m, as @ bs, ||as||, P Q, P & Q, x:A B(x), a < b, n - m, x:A. B(x), s = t, P Q, P Q, x:AB(x)

Lemmas select wf, length wf nat, top wf, true wf, squash wf, le wf, non neg length, cons one one, guard wf, nat wf, member wf, iff wf, rev implies wf, add functionality wrt eq, length append